Nuprl Lemma : pairwise_wf
11,40
postcript
pdf
T
:Type{i},
L
:(
T
List),
P
:(
T
T
prop{i':l}). pairwise(
x
,
y
.
P
(
x
,
y
);
L
)
prop{i':l}
latex
Definitions
x
:
A
.
B
(
x
)
,
prop{i:l}
,
t
T
,
pairwise(
x
,
y
.
P
(
x
;
y
);
L
)
,
x
(
s1
,
s2
)
,
P
Q
,
A
B
,
A
,
False
,
int_seg(
i
;
j
)
,
lelt(
i
;
j
;
k
)
,
P
Q
Lemmas
int
seg
wf
,
length
wf1
,
select
wf
origin
T:Type{i}, L:(T List), P:(T
Tprop{i':l}). pairwise(x,y.P(x,y); L) 
prop{i':l} T:Type{i}, L:(T List), P:(TTprop{i':l}). pairwise(x,y.P(x,y); L) prop{i':l} x:A. B(x) T
Q
B
A
Q